package checkers.oigj;

import javax.annotation.processing.*;
import javax.lang.model.element.AnnotationMirror;
import javax.lang.model.element.Element;

import com.sun.source.tree.ExpressionTree;
import com.sun.source.tree.Tree;

import checkers.basetype.BaseTypeChecker;
import checkers.oigj.quals.*;
import checkers.quals.TypeQualifiers;
import checkers.types.*;
import checkers.types.AnnotatedTypeMirror.AnnotatedDeclaredType;
import checkers.util.*;

/**
 * A type-checker plug-in for the OIGJ immutability type system that finds (and
 * verifies the absence of) undesired side-effect errors.
 *
 * The OIGJ language is a Java language extension that expresses
 * immutability constraints, using a few annotations: {@link
 * ReadOnly}, {@link OMutable}, {@link Immutable}, {@link OI} -- a
 * polymorphic qualifier, {@link Assignable}, and {@link
 * AssignsFields}, and some more introduced in 2009 to add ownership.
 * The language is specified by the FSE 2007 paper and another paper
 * being written in 2009.
 *
 * @manual #oigj-checker OIGJ Checker
 *
 */
@TypeQualifiers({ ReadOnly.class, Immutable.class, OI.class,
	    AssignsFields.class, OIGJBottom.class, OMutable.class, PrivateI.class,
	    PrivateMutable.class, PublicI.class, PublicMutable.class })
public class OIGJChecker extends BaseTypeChecker {
    //
    // OIGJ tries to adhere to the various rules specified by the
    // type system and the conventions of the framework, except for two
    // things:
    // 1. overloading the meaning of BOTTOM_QUAL
    //    Review the javadoc of #createQualiferHierarchy
    //
    // 2. Having two qualifiers for a given type in one particular case
    //    which is that the self type (i.e. type of 'this' identifier) within
    //    a method with an AssignsFields receiver within OI classes, then the self type is
    //    '@AssignsFields @OI EnclosingClass' and they are treated as
    //    Incomparable.  This is useful in the following cases:
    //
    //    a. for method invocability tests, a method with an AssignsFields receiver from within
    //       a readonly context can be called only via AssignsFields reference
    //       of 'this'.  OI cannot be a receiver type, so it doesn't interfere.
    //
    //    b. for assignment, 'this' can be assigned to '@OI EnclosingClass'
    //       reference within such methods (assignment encompasses the escape
    //       of this when passed to method parameters).  Fields and variables
    //       cannot be AssignsFields, so it's safe.
    //
    //    The design of QualifierHierarchy.isSubtype(Collection, Collection)
    //    reflect this choice.
    //
    /** Supported Annotations for OIGJ. Used for subtyping rules **/
    protected AnnotationMirror READONLY, IMMUTABLE, OI, ASSIGNS_FIELDS,
	BOTTOM_QUAL, OMUTABLE, PRIVATEI, PRIVATEMUTABLE, PUBLICI, PUBLICMUTABLE;

    @Override
    public synchronized void init(ProcessingEnvironment env) {
        AnnotationUtils annoFactory = new AnnotationUtils(env);
        READONLY = annoFactory.fromClass(ReadOnly.class);
        IMMUTABLE = annoFactory.fromClass(Immutable.class);
        OI = annoFactory.fromClass(OI.class);
        ASSIGNS_FIELDS = annoFactory.fromClass(AssignsFields.class);
        BOTTOM_QUAL = annoFactory.fromClass(OIGJBottom.class);
        OMUTABLE = annoFactory.fromClass(OMutable.class);
        PRIVATEI = annoFactory.fromClass(PrivateI.class);
        PRIVATEMUTABLE = annoFactory.fromClass(PrivateMutable.class);
        PUBLICI = annoFactory.fromClass(PublicI.class);
        PUBLICMUTABLE = annoFactory.fromClass(PublicMutable.class);
        super.init(env);
    }

    // **********************************************************************
    // OIGJ specific Type Relationship
    // **********************************************************************

    /**
     * Return true if the assignment variable is an assignable field or
     * variable, and returns false otherwise.
     *
     * A field is assignable if it is
     *
     * 1. a static field
     * 2. marked {@link Assignable}
     * 3. accessed through a mutable reference
     * 4. reassigned with an {@link AssignsFields} method and owned by 'this'
     *
     */
    @Override
    public boolean isAssignable(AnnotatedTypeMirror varType,
            AnnotatedTypeMirror receiverType, Tree varTree) {
        if (!(varTree instanceof ExpressionTree))
            return true;

	/*
	System.out.println("OIGJ DEBUG: Checking if " + varType + " is assignable to " +
			   receiverType + " with varTree = " + varTree);
	*/
		
        Element varElement = InternalUtils.symbol(varTree);
        if (varTree.getKind() != Tree.Kind.ARRAY_ACCESS
                && (varElement == null // a variable element should never be null
                        || !varElement.getKind().isField()
                        || ElementUtils.isStatic(varElement)
		    || varElement.getAnnotation(Assignable.class) != null)) {
            return true;
	}

	// Stop @PrivateI from being accessed in other ways than "this." or via @PrivateI.
	if (varType.hasAnnotation(PRIVATEI) && !receiverType.hasAnnotation(PRIVATEI)) {
	    // This can only be accessed using "this.".
	    if (!TreeUtils.isSelfAccess((ExpressionTree)varTree)) {
		return false;
	    }
	}

        assert receiverType != null;

        final boolean isAssignable =
            ((receiverType.hasAnnotation(OMUTABLE) ||
	      receiverType.hasAnnotation(PRIVATEMUTABLE) ||
	      receiverType.hasAnnotation(PUBLICMUTABLE))
             || receiverType.hasAnnotation(BOTTOM_QUAL)
             || (receiverType.hasAnnotation(ASSIGNS_FIELDS)
                     && TreeUtils.isSelfAccess((ExpressionTree)varTree)));

	if (!isAssignable) {
	    // FIXME: Allow @PrivateI through as if though it was
	    // mutable till it is resolved.
	    if (receiverType.hasAnnotation(PRIVATEI)) {
		return true;
	    }

	    // FIXME: Allow @PublicI through as if though it was
	    // mutable till it is resolved.
	    if (receiverType.hasAnnotation(PUBLICI)) {
		return true;
	    }

	    // FIXME: Allow @OI through as if though it was
	    // mutable till it is resolved.
	    if (receiverType.hasAnnotation(OI)) {
		return true;
	    }
	}
	
        return isAssignable;
    }

    @Override
    public boolean isValidUse(AnnotatedDeclaredType elemType, AnnotatedDeclaredType use) {
	/*
	if (use.hasAnnotation(PRIVATEI)) {
	    System.out.println("OIGJ DEBUG: inside isValidUse elemType = " + elemType +
			       " and use = " + use + " and use.getElement() = " +
			       use.getElement());
	}
	*/
	
        if (elemType.hasAnnotation(OI) || use.hasAnnotation(READONLY))
            return true;
        return super.isValidUse(elemType, use);
    }

    // **********************************************************************
    // Factory methods
    // **********************************************************************

    @Override
    protected QualifierHierarchy createQualifierHierarchy() {
        return new OIGJQualifierHierarchy((GraphQualifierHierarchy)
					  super.createQualifierHierarchy());
    }

    @Override
    protected TypeHierarchy createTypeHierarchy() {
        return new OIGJTypeHierarchy(getQualifierHierarchy());
    }

    //
    // OIGJ makes an interesting use of BOTTOM_QUAL (OIGJBottom).  It gets used
    // in two ways:
    //
    // __ AS BOTTOM QUALIFIER __
    //
    // This is the intended use and design for it
    //
    // A bottom qualifier is needed to annotate some expressions, like 'null'.
    // Otherwise, null would need to be '@OMutable @Immutable <nulltype>' so
    // it could be assigned to everything.
    //
    // __ AS SUPER QUALIFIER __
    //
    // As I used OIGJ, I realized that it's useful to have an annotation
    // that acts as a place holder qualifier that is a supertype of
    // everything.  The semantics of such qualifier is a bit
    // different from ReadOnly.
    //
    // It's only because the existence of un-annotated code that we need this
    // annotation, and OIGJ's promise that un-annotated code should type check.
    //
    // TODO: Explain these cases more
    //
    private final class OIGJQualifierHierarchy extends GraphQualifierHierarchy {
        public OIGJQualifierHierarchy(GraphQualifierHierarchy hierarchy) {
            super(hierarchy);
        }
        public boolean isSubtype(AnnotationMirror rhs, AnnotationMirror lhs) {
            return (AnnotationUtils.areSame(rhs, BOTTOM_QUAL)
                    || AnnotationUtils.areSame(lhs, BOTTOM_QUAL)
                    || super.isSubtype(rhs, lhs));
        }
    }

    /**
     * Represents the annotated type hierarchy of the OIGJ type system.
     *
     * The OIGJ type system diverges from the JLS in two ways:
     * 1. Type arguments are always co-variant with respect to
     *    {@link OIGJBottom}
     *
     * 2. If the type is a read-only or an immutable type, then type arguments
     *    may change co-variantly in a safe manner
     */
    private final class OIGJTypeHierarchy extends TypeHierarchy {
        public OIGJTypeHierarchy(QualifierHierarchy qualifierHierarchy) {
            super(qualifierHierarchy);
        }

        /**
         * Returns true if either of the provided types is a
         * {@link OIGJBottom}, otherwise uses the JLS specification
         * implemented by the abstract {@link typeHierarchy}.
         *
         */
        // Note: This cannot be expressed with the QualifierHierarchy alone,
        // as TypeHierarchy requires type arguments to be equivalent
        @Override
        protected boolean isSubtypeAsTypeArgument(AnnotatedTypeMirror rhs,
						  AnnotatedTypeMirror lhs) {
            return (lhs.hasAnnotation(BOTTOM_QUAL)
                    || rhs.hasAnnotation(BOTTOM_QUAL)
                    || super.isSubtypeAsTypeArgument(rhs, lhs));
        }


        /**
         * Uses the JLS specification (as implemented in {@link TypeHierarchy},
         * if the variable type, lhs, is mutable; otherwise, allows the type
         * arguments to change while maintaining subtype relationship.
         *
         * This allows for subtyping relationships of the kind:
         * <code>
         *  \@OMutable List<\@OMutable Date> <: \@ReadOnly List<@ReadOnly Date>
         * </code>
         */
        @Override
        protected boolean isSubtypeTypeArguments(AnnotatedDeclaredType rhs,
						 AnnotatedDeclaredType lhs) {
            if ((lhs.hasAnnotation(OMUTABLE) ||
		 lhs.hasAnnotation(PRIVATEMUTABLE) ||
		 lhs.hasAnnotation(PUBLICMUTABLE)))
                return super.isSubtypeTypeArguments(rhs, lhs);

            if (!lhs.getTypeArguments().isEmpty()
                    && !rhs.getTypeArguments().isEmpty()) {
                assert lhs.getTypeArguments().size() == rhs.getTypeArguments().size();
                for (int i = 0; i < lhs.getTypeArguments().size(); ++i) {
                    if (!isSubtype(rhs.getTypeArguments().get(i),
				   lhs.getTypeArguments().get(i)))
                        return false;
                }
            }
            return true;
        }
    }
}
